# FormalRV.Arithmetic Logical arithmetic gadgets (Cuccaro/Gidney adders, modular multiplier, unary lookup) and their semantic-correctness proofs. This umbrella imports every module under `Arithmetic/`.

(no documented top-level declarations)

FormalRV.Audit — one reader-facing audit file per paper. Each `FormalRV/Audit/<Paper>/` holds ONLY that paper's specific implementation + scheduling, and imports ONLY general/reusable code from the framework folders (`Shor`, `LatticeSurgery`, `QEC`, `System`, `PPM`, `Framework`, `Verifier`, …) — never another paper. Its layer files expose the relevant theorems with `#check` / `#verify_clean`, framed by a docstring that states the paper's headline claim, the SETTINGS a reader should check against the paper, OUR APPROACH, the GAP we determined, and what is STILL UNSOLVED. A reader verifies any single paper with, e.g., lake build FormalRV.Audit.Gidney2025 Compilation confirms every cited theorem type-checks; the `#print axioms` lines reveal the exact trust base. See FormalRV/Audit/README.md for the index table.

(no documented top-level declarations)

# FormalRV.Codegen Code-emission and the shared-syntax bridge: the `DEVICE-PROGRAM` serializer (`SysCallEmit`), its PARSER + backend-JSON reader (`DeviceProgramParse`, the Lean side of the Lean ↔ FTQ-VM interop loop), and the QASM serializers. This umbrella imports the library* codegen modules that are part of the umbrella `lake build`. The `#eval`-driven demo modules (`SysCallEmitDemo.lean`, `WindowedEmitDemo.lean`, the QASM demos) are intentionally NOT imported here — they print on elaboration and are run on demand with `lake env lean <file>`.

(no documented top-level declarations)

# FormalRV.Core Definitions: the Gate IR, classical & quantum (matrix) semantics, gate decompositions. This umbrella imports every module under `Core/`.

(no documented top-level declarations)

# FormalRV.Framework The four inter-layer contract interfaces (L1 algorithm, L2 gadgets, L3 PPM, L4 QEC code) + error mechanisms. This umbrella imports every module under `Framework/`.

(no documented top-level declarations)

FormalRV.NumberTheory — the classical number theory Shor's algorithm needs to FACTOR. Shor's quantum subroutine finds the multiplicative order `r` of `a` mod `N` (`FormalRV.SQIRPort.Shor_correct_var`). Turning that order into a FACTOR of `N` is pure classical number theory, previously absent from this repo (`Framework.L1_Algorithm.rsa_correct : True`). This folder supplies it, separating PROVEN mathematics from genuinely-conjectural assumptions. PROVEN (all axiom-clean `[propext, Classical.choice, Quot.sound]`): `NontrivialSqrt` — a nontrivial square root of 1 mod N yields a nontrivial factor via gcd. `OrderToFactor` — even order `r` with `a^(r/2) ≢ −1` yields a nontrivial factor (`order_even_factor`); plus the common-factor easy case. `ShorReduction` — `shor_classical_step_correct` (the order→factor reduction) and `nontrivialSqrt_exists` / `factor_of_coprime_split` (non-vacuity via CRT: a factor-witness always exists for a coprime non-prime-power split). `GoodElements` — the Shor/Miller `≥ 1/2` COUNTING, in full: in any finite cyclic group of even order every `v₂(ord)`-atom is `≤ |G|/2` (`card_atom_le_half`); for a product `G × H` the `v₂`-diagonal is `≤ |G×H|/2` (`card_diag_v2_le_half`); the "bad" set IS that diagonal (`prodBad_iff_diag`, via `orderOf` = lcm and `v₂`(lcm) = max), so `card_prodBad_le_half`. `ShorBadSet` — the `≥ 1/2` bound TRANSPORTED to `(ℤ/N)ˣ` for `N = p·q` (distinct odd primes) via the CRT iso + the field square-root dichotomy `s^(r/2) = −1 ↔ s^(r/2) ≠ 1`: `card_bad_le_half` (`|{a : ord a odd ∨ a^(ord a/2) = −1}| ≤ φ(N)/2`) and its complement `card_good_ge_half` (a uniformly random unit is good — yields a factor — with probability ≥ 1/2). REMAINING (genuinely conjectural — NOT proven, never faked): `FormalRV.CFS.SmallPrimeRNSModulusExists` (Gidney 2025 / CFS prime-set + modular-deviation conjecture) and the Ekerå-2023 short-DLP success lemmas — the papers themselves leave these conjectural / give only analytic bounds; they remain explicit named assumptions, not theorems.

(no documented top-level declarations)

FormalRV.PPM — the Pauli-Product-Measurement layer, organised as a hierarchy: Syntax/ — the PPM IR: Pauli / PauliString / PPM / PPMCommand data types + syntactic ops Semantics/ — state-vector & operational semantics, denotation, observation bridges Rules/ — Clifford conjugation & rewrite laws, ZX Compiler/ — circuit -> PPM lowering, its correctness, and backend trace lowering Magic/ — magic-state teleportation gadgets & Toffoli/CCZ magic schemes Resource/ — PPM-level resource counters + anchored count theorems QECBridge/ — PPM <-> QEC layering & magic-factory provisioning interfaces Gadgets/ — per-gadget compiled-PPM semantic correctness vs the compiler contract Pipeline/ — Shor end-to-end assemblies + paper-specific instantiations Codegen/ — PPM -> OpenQASM text emission See PPM/README.md for the layer map and the honesty boundaries.

(no documented top-level declarations)

FormalRV.PauliRotation — umbrella. The Pauli-rotation IR: the standard (Litinski) layer between the logical circuit IRs and PPM programs. Circuits compile to ±{π, π/2, π/4, π/8} Pauli-product rotations, commuting rotations group into PARALLEL layers (depth = layer count), and the layers lower to PPM. Folder map (see `PauliRotation/README.md`): Syntax.lean — THE IR: `Rot`/`RotLayer`/`RotProg`, `commF`, wf Semantics/ — THE MEANING: `rotOf` algebra, `axisMat`, denotations, the commutation bridge, basis actions, the phase-tracked Pauli product Compiler/ — THE COMPILERS: gate dictionary, schedulers (greedy + hardware-K-bounded), rewrite rules, Clifford pushing, the certificate-checked optimizer; `ToPPM/` lowers rotations to PPM measurement programs Correctness/ — THE PROOFS that compiled programs equal the gate unitaries (dictionary rows → assembly → Shor) Gadgets/ — per-arithmetic-gadget instances

(no documented top-level declarations)

# FormalRV.QEC The QEC layer: the *demand side* of fault-tolerant Shor, assuming infinitely many *virtual qubits** (no hardware mapping, no system calls — those live in `FormalRV.System`, the supply side that answers whether a finite machine can run this in a given time). Contents: GF(2) toolkit + code mathematics (CSS codes, code families surface/HGP/BB/LP, logical operators, code dimension). `LatticeSurgery/` — lattice-surgery gadgets over arbitrary CSS codes: syntax (`SurgeryGadget`), decidable structural verification, stabilizer semantics (the gadget implements the target logical Pauli measurement), schedules, resource counts (incl. per-check syndrome ancillas), and Stim emitters. This umbrella imports every module under `QEC/`.

(no documented top-level declarations)

FormalRV.QFT — the inverse Quantum Fourier Transform (IQFT), the measurement-basis transform of QPE / Shor, as a VERIFIED `BaseUCom` circuit. Extracted from Shor/ as a general, Shor-agnostic component (sibling of QPE/). ## The spine (read these four) • `IQFTDef` — THE definition: `IQFT n` (= `real_QFTinv_layer n` = framework `BaseUCom.QFTinv n`) + the ideal `IQFT_matrix`. • `IQFTCorrectness` — THE main theorem: `uc_eval (IQFT n) = IQFT_matrix n` for all `n ≥ 1` (`iqft_correct`), + the framework bridge. • `IQFTResource` — the cost/compilation story: banded (approximate) QFT is exactly Clifford+T, with the derived `≤ 2π/2^c` error budget. • `IQFTExample` — worked 2- and 3-qubit example + uniform `emitQASM` (`IQFTGadget`); kept OFF the default build path (#evals). Supporting proofs (imported by the spine; read only when auditing the proofs): `IQFTRecursiveArbitrary` (arbitrary-n column induction), `IQFTCircuitCorrectness` (1- and 2-qubit base cases + lemmas), `AQFTCompile` / `AQFTCompileSemantics` (the Clifford+T compiler), and `IQFTDefinitions` (the helper defs the proofs run on). See `README.md` for the qubit layout, the worked example, and the diagram.

(no documented top-level declarations)

FormalRV.QPE — Quantum Phase Estimation, over an ABSTRACT (black-box) oracle. Extracted from Shor/ as a general, oracle-generic component (sibling of QFT/). ## The spine (read these four) • `QPEDef` — THE definition: `QPE k n c` (= npar_H ; controlled_powers c ; QFTinv) with `c` a BLACK-BOX oracle family; `qpe_phase_state`. • `QPECorrectness` — THE main theorem: `qpe_on_eigenstate_correct` — QPE on an eigenstate of the abstract oracle yields the phase state (relocated here out of QFT/; modexp-free, oracle-generic). • `QPEResource` — the only QPE overhead is the H-layer + the inverse-QFT measurement basis (Clifford+T compilation + error budget). • `QPEExample` — worked phase-oracle example + uniform `emitQASM` (`QPEPhaseGadget`); kept OFF the default build path (#evals). Supporting machinery (imported by the spine; read only when auditing proofs): `PhaseKickback` (the phase-kickback cascade + pre-QFT Fourier form), `ControlledGates` (controlled-gate semantics + the `control` decomposition), `QPEAmplitude` (Dirichlet-kernel amplitude analysis + the 4/π² peak bound), and `QPE` (the circuit definitions). Modular exponentiation is NOT QPE's job — it is a black-box oracle here; its instantiation lives in Shor (`Shor/PostQFT/QPEModmultEigenstate.lean`). See `README.md` for the qubit layout, the worked example, and the diagram.

(no documented top-level declarations)

# FormalRV.Qualtran Data bridge mirroring Qualtran's PhysicalParameters into Lean. This umbrella imports every module under `Qualtran/`.

(no documented top-level declarations)

FormalRV.Resource — the SEPARATE, INDEPENDENT resource-counting system. ## Why a separate folder A resource count must be an honest tree-walk over a syntactic object and NOTHING else. Everything in this folder imports ONLY the circuit IRs (`Gate`, `BaseUCom`, …) — never the gadget constructors and never the correctness proofs. Because the counters live in their own world, a resource theorem `countT (gadget n) = 14·n` cannot fudge the count: the number is forced by the syntax tree, and a skeptic can `#eval` the counter on a constructed circuit to check it WITHOUT reading any proof. ## The verification shape this enforces Each verified resource claim carries a TRIPLE: (1) a concrete syntactic object (or a generator that builds it), (2) a proof it is semantically correct against the spec, and (3) a proof that THESE counters, applied to THAT object, equal the closed form. No formula like `3n` is ever asserted without a real object behind it. The per-gadget count THEOREMS (item 3) live with their gadget (e.g. `Arithmetic/Cuccaro/CuccaroAdderResource.lean`, `QFT/IQFTResource.lean`); this folder owns the COUNTERS they use. ## Contents • `GateCount` — TIME `countT` / `countCNOT` / `countToffoli` / `countX` / `gateCount` / `depth` + SPACE `width`, on the reversible `Gate` IR (with bridges to the legacy `Gate.tcount` / `gcount`). • `UComCount` — TIME `gateCountU` / `cnotCountU` / `oneQCountU` + SPACE `widthU`, on the unitary `BaseUCom` IR (the QFT/QPE counters — previously ABSENT). • `UComCombinators` — count laws for the core combinators (`SWAP`, `CCX`, `controlled_R`, `control`, `npar`, `npar_H`) — what lets a structured circuit's count reduce to its parts'. • `Interface` — the `HasResourceCount` typeclass unifying the IRs (`cnot`, `gates` = time; `qubits` = space). • `QECCircuitCount` — TIME `cxCountC` / `measCountC` / `prepCountC` / `opCountC` + SPACE `widthC`, on the QEC physical- circuit IR (`QEC/Circuit/PhysCircuit.lean`) — the layer at which syndrome/surgery-ancilla overhead is explicit in the syntax tree and therefore counted. Per-gadget closed-form count theorems live with their gadgets: `Arithmetic/*Resource*.lean` (Gate IR), `QFT/IQFTCount.lean` (the inverse QFT: CNOTs = 3⌊n/2⌋+n(n−1), qubits = n), `QPE/QPECount.lean` (QPE over a black-box oracle), `QEC/Circuit/ExtractionCount.lean` (the compiled syndrome-extraction circuit of a surgery gadget: width = `surgeryPhysQubits`, CNOTs = `surgeryCNOTs`, measurements = `surgeryMeasPerRound`/`surgeryTotalMeas`). • `SysCallCount` — the SYSTEM (L4) layer, on `List SysCall`: TIME `wallclockUs` / `totalBusyUs` + per-kind op counters (`countGate2q`, `countMeasure`, `countDecode`, `countMagicReq`, …); SPACE `qubitFootprint` / `peakSiteOccupancy` (sites via `syscall_acts_on`); channel ids `decodeIds` / `pfuCorrs`; syndrome volume `syndromeBitsTotal`. Consumers re-pointed to these (the wallclock alias `scheduleWallclockUs`, `resourceOfSysCalls`'s fields, `FTSchedule.countKind`, the GE2021 PPM block counts) — no parallel counting walks remain at the SysCall level. The FTQ-VM computes the same quantities independently from the same DEVICE-PROGRAM files (`test_resource_counts.py`). Migration TODO (tracked): re-home the PPM measurement/magic-T counters (`ppmProgramResourceSummary`, `numMeas`) and the system `CostModel` under this folder behind the same `HasResourceCount`-style interface. (The lattice- surgery gadget-field counters are now THEOREM-tied to the syntactic extraction circuit via `QEC/Circuit/ExtractionCount.lean`.)

(no documented top-level declarations)

# FormalRV.Shor The main result: Shor order-finding success probability (see `Shor/Main.lean`), QPE, phase kickback, inverse-QFT. This umbrella imports every module under `Shor/`.

(no documented top-level declarations)

# FormalRV.System System invariants: scheduling, layout, architecture, capacity/latency/bandwidth checks. This umbrella imports every module under `System/`. Layout (post 2026-06-11 reorg, see `System/VM_AUDIT.md` §4): - `Core/` — `Architecture` (Zone/Channel/SysCall IR), `CodedLayout` (+ `syscall_acts_on`) - `Invariants/` — decidable I1–I4 checkers and the strengthened bundles - `Checkers/` — `SystemChecker` (adversarial gap audit), `FaultTolerantSchedule` - `DeviceLane/` — the parallel `DeviceOp` schedule engine + routing + dependency graphs - `Decoder/` — decoder backlog/reaction/syndrome-latency rate models - `Magic/` — magic-state readiness and whole-circuit wait laws - `Bounds/` — lower floors, naive ceilings, hardware sensitivity - `Compile/` — surgery-gadget → SysCall compilation and full surface-Shor schedules - `Artifacts/` — layered artifact/certificate interface, compressed-repeat soundness (the landing zone for the FTQ-VM `certificate.json` checker) - `Examples/` — worked invariant examples and demo instances - `Params/` — hardware parameter records and zone budgets *Single entry point:** `FormalRV.System.FTFramework` is the coherent front door tying the two scheduling subsystems together — canonical hardware (`HardwareParams.MachineParams`, one decoder- reaction budget), schedule well-formedness (`DeviceSchedule.scheduleValid` / `ScheduleInv.all_invariants_ok`), the resource BRACKET (`ScheduleBounds.resource_bracket`: lower floor ≤ workload ≤ upper ceiling, with `naive_peak_le_total` the peak ≤ footprint upper bound), and hardware SENSITIVITY (`HardwareSensitivity.HW.timeLB`). The two naive efforts (`NaiveSchedule` over `DSchedule`, `NaiveUpperBound` over `ResourceEstimate`) and the two checkers (`DeviceSchedule` over `DeviceOp`, `InvariantFramework` over `SysCall`) are connected by theorems, not merged.

(no documented top-level declarations)

# FormalRV.Verifier The verifier: an airtight, user-fixed specification of a correct Shor implementation on a user-supplied LP code, plus the `#verify_clean` enforcement gate that REJECTS any submission which is incomplete (`sorry`) or leans on an extra axiom. Set the spec first; build the construction second; the gate decides acceptance.

(no documented top-level declarations)